YES 1.27
↳ HASKELL
↳ LR
((scanr1 :: (a -> a -> a) -> [a] -> [a]) :: (a -> a -> a) -> [a] -> [a]) |
import qualified Prelude |
\qs→qs
qs0 qs = qs
\(q : _)→q
q1 (q : _) = q
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
((scanr1 :: (a -> a -> a) -> [a] -> [a]) :: (a -> a -> a) -> [a] -> [a]) |
import qualified Prelude |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
((scanr1 :: (a -> a -> a) -> [a] -> [a]) :: (a -> a -> a) -> [a] -> [a]) |
import qualified Prelude |
undefined
| False
= undefined
undefined = undefined1
undefined0 True = undefined
undefined1 = undefined0 False
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
((scanr1 :: (a -> a -> a) -> [a] -> [a]) :: (a -> a -> a) -> [a] -> [a]) |
import qualified Prelude |
f x q : qs where
q = q1 vu41
q1 (q : vv) = q
qs = qs0 vu41
qs0 qs = qs
vu41 = scanr1 f xs
scanr1Q vy vz = scanr1Q1 vy vz (scanr1Vu41 vy vz)
scanr1Qs0 vy vz qs = qs
scanr1Vu41 vy vz = scanr1 vy vz
scanr1Q1 vy vz (q : vv) = q
scanr1Qs vy vz = scanr1Qs0 vy vz (scanr1Vu41 vy vz)
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
(scanr1 :: (a -> a -> a) -> [a] -> [a]) |
import qualified Prelude |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ QDP
↳ RuleRemovalProof
new_scanr1(wu3, :(wu40, :(wu410, wu411)), ba) → new_scanr1(wu3, :(wu410, wu411), ba)
new_scanr1Vu41(wu3, wu410, wu411, ba) → new_scanr1(wu3, :(wu410, wu411), ba)
new_scanr1(wu3, :(wu40, :(wu410, wu411)), ba) → new_scanr1Vu41(wu3, wu410, wu411, ba)
new_scanr1(wu3, :(wu40, :(wu410, wu411)), ba) → new_scanr1(wu3, :(wu410, wu411), ba)
new_scanr1(wu3, :(wu40, :(wu410, wu411)), ba) → new_scanr1Vu41(wu3, wu410, wu411, ba)
POL(:(x1, x2)) = 2 + 2·x1 + x2
POL(new_scanr1(x1, x2, x3)) = x1 + x2 + x3
POL(new_scanr1Vu41(x1, x2, x3, x4)) = 2 + x1 + 2·x2 + x3 + x4
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
new_scanr1Vu41(wu3, wu410, wu411, ba) → new_scanr1(wu3, :(wu410, wu411), ba)